0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇒, 289 ms)
↳2 Prolog
↳3 PrologToPiTRSProof (⇒, 53 ms)
↳4 PiTRS
↳5 DependencyPairsProof (⇔, 257 ms)
↳6 PiDP
↳7 DependencyGraphProof (⇔, 0 ms)
↳8 AND
↳9 PiDP
↳10 UsableRulesProof (⇔, 0 ms)
↳11 PiDP
↳12 PiDPToQDPProof (⇔, 0 ms)
↳13 QDP
↳14 QDPSizeChangeProof (⇔, 0 ms)
↳15 YES
↳16 PiDP
↳17 UsableRulesProof (⇔, 0 ms)
↳18 PiDP
↳19 PiDPToQDPProof (⇔, 0 ms)
↳20 QDP
↳21 QDPSizeChangeProof (⇔, 0 ms)
↳22 YES
↳23 PiDP
↳24 UsableRulesProof (⇔, 0 ms)
↳25 PiDP
↳26 PiDPToQDPProof (⇒, 24 ms)
↳27 QDP
↳28 QDPSizeChangeProof (⇔, 0 ms)
↳29 YES
insertC_in_gga(T5, void, tree(T5, void, void)) → insertC_out_gga(T5, void, tree(T5, void, void))
insertC_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertC_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertC_in_gga(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21)) → U6_gga(T28, T20, T21, T23, pB_in_gga(T28, T20, T23))
pB_in_gga(T28, T20, T23) → U2_gga(T28, T20, T23, lessA_in_g(T28))
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U2_gga(T28, T20, T23, lessA_out_g(T28)) → pB_out_gga(T28, T20, T23)
U2_gga(T28, T20, T23, lessA_out_g(T28)) → U3_gga(T28, T20, T23, insertC_in_gga(s(T28), T20, T23))
insertC_in_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46)) → U7_gga(T42, T43, T44, T46, lessA_in_g(T42))
U7_gga(T42, T43, T44, T46, lessA_out_g(T42)) → insertC_out_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46))
U7_gga(T42, T43, T44, T46, lessA_out_g(T42)) → U8_gga(T42, T43, T44, T46, insertC_in_gga(T42, T44, T46))
insertC_in_gga(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57)) → U9_gga(T60, T54, T55, T57, pB_in_gga(T60, T55, T57))
U9_gga(T60, T54, T55, T57, pB_out_gga(T60, T55, T57)) → insertC_out_gga(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57))
insertC_in_gga(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69)) → U10_gga(T76, T68, T69, T71, insertC_in_gga(0, T68, T71))
insertC_in_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69)) → U11_gga(T85, T86, T68, T69, T71, lessE_in_gg(T85, T86))
lessE_in_gg(0, s(T95)) → lessE_out_gg(0, s(T95))
lessE_in_gg(s(0), s(s(T108))) → lessE_out_gg(s(0), s(s(T108)))
lessE_in_gg(s(s(0)), s(s(s(T121)))) → lessE_out_gg(s(s(0)), s(s(s(T121))))
lessE_in_gg(s(s(s(0))), s(s(s(s(T134))))) → lessE_out_gg(s(s(s(0))), s(s(s(s(T134)))))
lessE_in_gg(s(s(s(s(0)))), s(s(s(s(s(T147)))))) → lessE_out_gg(s(s(s(s(0)))), s(s(s(s(s(T147))))))
lessE_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160))))))) → lessE_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160)))))))
lessE_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173)))))))) → lessE_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173))))))))
lessE_in_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179)))))))) → U5_gg(T178, T179, lessD_in_gg(T178, T179))
lessD_in_gg(0, s(T190)) → lessD_out_gg(0, s(T190))
lessD_in_gg(s(T195), s(T196)) → U4_gg(T195, T196, lessD_in_gg(T195, T196))
U4_gg(T195, T196, lessD_out_gg(T195, T196)) → lessD_out_gg(s(T195), s(T196))
U5_gg(T178, T179, lessD_out_gg(T178, T179)) → lessE_out_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179))))))))
U11_gga(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → insertC_out_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69))
U11_gga(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → U12_gga(T85, T86, T68, T69, T71, insertC_in_gga(s(T85), T68, T71))
insertC_in_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216)) → U13_gga(T211, T212, T213, T214, T216, lessD_in_gg(T212, T211))
U13_gga(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → insertC_out_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216))
U13_gga(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → U14_gga(T211, T212, T213, T214, T216, insertC_in_gga(T211, T214, T216))
insertC_in_gga(s(T238), tree(0, T230, T231), tree(0, T230, T233)) → U15_gga(T238, T230, T231, T233, insertC_in_gga(s(T238), T231, T233))
insertC_in_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233)) → U16_gga(T246, T245, T230, T231, T233, lessD_in_gg(T245, T246))
U16_gga(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → insertC_out_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233))
U16_gga(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → U17_gga(T246, T245, T230, T231, T233, insertC_in_gga(s(T246), T231, T233))
U17_gga(T246, T245, T230, T231, T233, insertC_out_gga(s(T246), T231, T233)) → insertC_out_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233))
U15_gga(T238, T230, T231, T233, insertC_out_gga(s(T238), T231, T233)) → insertC_out_gga(s(T238), tree(0, T230, T231), tree(0, T230, T233))
U14_gga(T211, T212, T213, T214, T216, insertC_out_gga(T211, T214, T216)) → insertC_out_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216))
U12_gga(T85, T86, T68, T69, T71, insertC_out_gga(s(T85), T68, T71)) → insertC_out_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69))
U10_gga(T76, T68, T69, T71, insertC_out_gga(0, T68, T71)) → insertC_out_gga(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69))
U8_gga(T42, T43, T44, T46, insertC_out_gga(T42, T44, T46)) → insertC_out_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46))
U3_gga(T28, T20, T23, insertC_out_gga(s(T28), T20, T23)) → pB_out_gga(T28, T20, T23)
U6_gga(T28, T20, T21, T23, pB_out_gga(T28, T20, T23)) → insertC_out_gga(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21))
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
insertC_in_gga(T5, void, tree(T5, void, void)) → insertC_out_gga(T5, void, tree(T5, void, void))
insertC_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertC_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertC_in_gga(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21)) → U6_gga(T28, T20, T21, T23, pB_in_gga(T28, T20, T23))
pB_in_gga(T28, T20, T23) → U2_gga(T28, T20, T23, lessA_in_g(T28))
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U2_gga(T28, T20, T23, lessA_out_g(T28)) → pB_out_gga(T28, T20, T23)
U2_gga(T28, T20, T23, lessA_out_g(T28)) → U3_gga(T28, T20, T23, insertC_in_gga(s(T28), T20, T23))
insertC_in_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46)) → U7_gga(T42, T43, T44, T46, lessA_in_g(T42))
U7_gga(T42, T43, T44, T46, lessA_out_g(T42)) → insertC_out_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46))
U7_gga(T42, T43, T44, T46, lessA_out_g(T42)) → U8_gga(T42, T43, T44, T46, insertC_in_gga(T42, T44, T46))
insertC_in_gga(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57)) → U9_gga(T60, T54, T55, T57, pB_in_gga(T60, T55, T57))
U9_gga(T60, T54, T55, T57, pB_out_gga(T60, T55, T57)) → insertC_out_gga(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57))
insertC_in_gga(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69)) → U10_gga(T76, T68, T69, T71, insertC_in_gga(0, T68, T71))
insertC_in_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69)) → U11_gga(T85, T86, T68, T69, T71, lessE_in_gg(T85, T86))
lessE_in_gg(0, s(T95)) → lessE_out_gg(0, s(T95))
lessE_in_gg(s(0), s(s(T108))) → lessE_out_gg(s(0), s(s(T108)))
lessE_in_gg(s(s(0)), s(s(s(T121)))) → lessE_out_gg(s(s(0)), s(s(s(T121))))
lessE_in_gg(s(s(s(0))), s(s(s(s(T134))))) → lessE_out_gg(s(s(s(0))), s(s(s(s(T134)))))
lessE_in_gg(s(s(s(s(0)))), s(s(s(s(s(T147)))))) → lessE_out_gg(s(s(s(s(0)))), s(s(s(s(s(T147))))))
lessE_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160))))))) → lessE_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160)))))))
lessE_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173)))))))) → lessE_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173))))))))
lessE_in_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179)))))))) → U5_gg(T178, T179, lessD_in_gg(T178, T179))
lessD_in_gg(0, s(T190)) → lessD_out_gg(0, s(T190))
lessD_in_gg(s(T195), s(T196)) → U4_gg(T195, T196, lessD_in_gg(T195, T196))
U4_gg(T195, T196, lessD_out_gg(T195, T196)) → lessD_out_gg(s(T195), s(T196))
U5_gg(T178, T179, lessD_out_gg(T178, T179)) → lessE_out_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179))))))))
U11_gga(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → insertC_out_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69))
U11_gga(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → U12_gga(T85, T86, T68, T69, T71, insertC_in_gga(s(T85), T68, T71))
insertC_in_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216)) → U13_gga(T211, T212, T213, T214, T216, lessD_in_gg(T212, T211))
U13_gga(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → insertC_out_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216))
U13_gga(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → U14_gga(T211, T212, T213, T214, T216, insertC_in_gga(T211, T214, T216))
insertC_in_gga(s(T238), tree(0, T230, T231), tree(0, T230, T233)) → U15_gga(T238, T230, T231, T233, insertC_in_gga(s(T238), T231, T233))
insertC_in_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233)) → U16_gga(T246, T245, T230, T231, T233, lessD_in_gg(T245, T246))
U16_gga(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → insertC_out_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233))
U16_gga(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → U17_gga(T246, T245, T230, T231, T233, insertC_in_gga(s(T246), T231, T233))
U17_gga(T246, T245, T230, T231, T233, insertC_out_gga(s(T246), T231, T233)) → insertC_out_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233))
U15_gga(T238, T230, T231, T233, insertC_out_gga(s(T238), T231, T233)) → insertC_out_gga(s(T238), tree(0, T230, T231), tree(0, T230, T233))
U14_gga(T211, T212, T213, T214, T216, insertC_out_gga(T211, T214, T216)) → insertC_out_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216))
U12_gga(T85, T86, T68, T69, T71, insertC_out_gga(s(T85), T68, T71)) → insertC_out_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69))
U10_gga(T76, T68, T69, T71, insertC_out_gga(0, T68, T71)) → insertC_out_gga(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69))
U8_gga(T42, T43, T44, T46, insertC_out_gga(T42, T44, T46)) → insertC_out_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46))
U3_gga(T28, T20, T23, insertC_out_gga(s(T28), T20, T23)) → pB_out_gga(T28, T20, T23)
U6_gga(T28, T20, T21, T23, pB_out_gga(T28, T20, T23)) → insertC_out_gga(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21))
INSERTC_IN_GGA(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21)) → U6_GGA(T28, T20, T21, T23, pB_in_gga(T28, T20, T23))
INSERTC_IN_GGA(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21)) → PB_IN_GGA(T28, T20, T23)
PB_IN_GGA(T28, T20, T23) → U2_GGA(T28, T20, T23, lessA_in_g(T28))
PB_IN_GGA(T28, T20, T23) → LESSA_IN_G(T28)
LESSA_IN_G(s(T31)) → U1_G(T31, lessA_in_g(T31))
LESSA_IN_G(s(T31)) → LESSA_IN_G(T31)
U2_GGA(T28, T20, T23, lessA_out_g(T28)) → U3_GGA(T28, T20, T23, insertC_in_gga(s(T28), T20, T23))
U2_GGA(T28, T20, T23, lessA_out_g(T28)) → INSERTC_IN_GGA(s(T28), T20, T23)
INSERTC_IN_GGA(T42, tree(T42, T43, T44), tree(T42, T43, T46)) → U7_GGA(T42, T43, T44, T46, lessA_in_g(T42))
INSERTC_IN_GGA(T42, tree(T42, T43, T44), tree(T42, T43, T46)) → LESSA_IN_G(T42)
U7_GGA(T42, T43, T44, T46, lessA_out_g(T42)) → U8_GGA(T42, T43, T44, T46, insertC_in_gga(T42, T44, T46))
U7_GGA(T42, T43, T44, T46, lessA_out_g(T42)) → INSERTC_IN_GGA(T42, T44, T46)
INSERTC_IN_GGA(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57)) → U9_GGA(T60, T54, T55, T57, pB_in_gga(T60, T55, T57))
INSERTC_IN_GGA(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57)) → PB_IN_GGA(T60, T55, T57)
INSERTC_IN_GGA(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69)) → U10_GGA(T76, T68, T69, T71, insertC_in_gga(0, T68, T71))
INSERTC_IN_GGA(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69)) → INSERTC_IN_GGA(0, T68, T71)
INSERTC_IN_GGA(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69)) → U11_GGA(T85, T86, T68, T69, T71, lessE_in_gg(T85, T86))
INSERTC_IN_GGA(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69)) → LESSE_IN_GG(T85, T86)
LESSE_IN_GG(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179)))))))) → U5_GG(T178, T179, lessD_in_gg(T178, T179))
LESSE_IN_GG(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179)))))))) → LESSD_IN_GG(T178, T179)
LESSD_IN_GG(s(T195), s(T196)) → U4_GG(T195, T196, lessD_in_gg(T195, T196))
LESSD_IN_GG(s(T195), s(T196)) → LESSD_IN_GG(T195, T196)
U11_GGA(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → U12_GGA(T85, T86, T68, T69, T71, insertC_in_gga(s(T85), T68, T71))
U11_GGA(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → INSERTC_IN_GGA(s(T85), T68, T71)
INSERTC_IN_GGA(T211, tree(T212, T213, T214), tree(T212, T213, T216)) → U13_GGA(T211, T212, T213, T214, T216, lessD_in_gg(T212, T211))
INSERTC_IN_GGA(T211, tree(T212, T213, T214), tree(T212, T213, T216)) → LESSD_IN_GG(T212, T211)
U13_GGA(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → U14_GGA(T211, T212, T213, T214, T216, insertC_in_gga(T211, T214, T216))
U13_GGA(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → INSERTC_IN_GGA(T211, T214, T216)
INSERTC_IN_GGA(s(T238), tree(0, T230, T231), tree(0, T230, T233)) → U15_GGA(T238, T230, T231, T233, insertC_in_gga(s(T238), T231, T233))
INSERTC_IN_GGA(s(T238), tree(0, T230, T231), tree(0, T230, T233)) → INSERTC_IN_GGA(s(T238), T231, T233)
INSERTC_IN_GGA(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233)) → U16_GGA(T246, T245, T230, T231, T233, lessD_in_gg(T245, T246))
INSERTC_IN_GGA(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233)) → LESSD_IN_GG(T245, T246)
U16_GGA(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → U17_GGA(T246, T245, T230, T231, T233, insertC_in_gga(s(T246), T231, T233))
U16_GGA(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → INSERTC_IN_GGA(s(T246), T231, T233)
insertC_in_gga(T5, void, tree(T5, void, void)) → insertC_out_gga(T5, void, tree(T5, void, void))
insertC_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertC_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertC_in_gga(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21)) → U6_gga(T28, T20, T21, T23, pB_in_gga(T28, T20, T23))
pB_in_gga(T28, T20, T23) → U2_gga(T28, T20, T23, lessA_in_g(T28))
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U2_gga(T28, T20, T23, lessA_out_g(T28)) → pB_out_gga(T28, T20, T23)
U2_gga(T28, T20, T23, lessA_out_g(T28)) → U3_gga(T28, T20, T23, insertC_in_gga(s(T28), T20, T23))
insertC_in_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46)) → U7_gga(T42, T43, T44, T46, lessA_in_g(T42))
U7_gga(T42, T43, T44, T46, lessA_out_g(T42)) → insertC_out_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46))
U7_gga(T42, T43, T44, T46, lessA_out_g(T42)) → U8_gga(T42, T43, T44, T46, insertC_in_gga(T42, T44, T46))
insertC_in_gga(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57)) → U9_gga(T60, T54, T55, T57, pB_in_gga(T60, T55, T57))
U9_gga(T60, T54, T55, T57, pB_out_gga(T60, T55, T57)) → insertC_out_gga(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57))
insertC_in_gga(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69)) → U10_gga(T76, T68, T69, T71, insertC_in_gga(0, T68, T71))
insertC_in_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69)) → U11_gga(T85, T86, T68, T69, T71, lessE_in_gg(T85, T86))
lessE_in_gg(0, s(T95)) → lessE_out_gg(0, s(T95))
lessE_in_gg(s(0), s(s(T108))) → lessE_out_gg(s(0), s(s(T108)))
lessE_in_gg(s(s(0)), s(s(s(T121)))) → lessE_out_gg(s(s(0)), s(s(s(T121))))
lessE_in_gg(s(s(s(0))), s(s(s(s(T134))))) → lessE_out_gg(s(s(s(0))), s(s(s(s(T134)))))
lessE_in_gg(s(s(s(s(0)))), s(s(s(s(s(T147)))))) → lessE_out_gg(s(s(s(s(0)))), s(s(s(s(s(T147))))))
lessE_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160))))))) → lessE_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160)))))))
lessE_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173)))))))) → lessE_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173))))))))
lessE_in_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179)))))))) → U5_gg(T178, T179, lessD_in_gg(T178, T179))
lessD_in_gg(0, s(T190)) → lessD_out_gg(0, s(T190))
lessD_in_gg(s(T195), s(T196)) → U4_gg(T195, T196, lessD_in_gg(T195, T196))
U4_gg(T195, T196, lessD_out_gg(T195, T196)) → lessD_out_gg(s(T195), s(T196))
U5_gg(T178, T179, lessD_out_gg(T178, T179)) → lessE_out_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179))))))))
U11_gga(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → insertC_out_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69))
U11_gga(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → U12_gga(T85, T86, T68, T69, T71, insertC_in_gga(s(T85), T68, T71))
insertC_in_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216)) → U13_gga(T211, T212, T213, T214, T216, lessD_in_gg(T212, T211))
U13_gga(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → insertC_out_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216))
U13_gga(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → U14_gga(T211, T212, T213, T214, T216, insertC_in_gga(T211, T214, T216))
insertC_in_gga(s(T238), tree(0, T230, T231), tree(0, T230, T233)) → U15_gga(T238, T230, T231, T233, insertC_in_gga(s(T238), T231, T233))
insertC_in_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233)) → U16_gga(T246, T245, T230, T231, T233, lessD_in_gg(T245, T246))
U16_gga(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → insertC_out_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233))
U16_gga(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → U17_gga(T246, T245, T230, T231, T233, insertC_in_gga(s(T246), T231, T233))
U17_gga(T246, T245, T230, T231, T233, insertC_out_gga(s(T246), T231, T233)) → insertC_out_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233))
U15_gga(T238, T230, T231, T233, insertC_out_gga(s(T238), T231, T233)) → insertC_out_gga(s(T238), tree(0, T230, T231), tree(0, T230, T233))
U14_gga(T211, T212, T213, T214, T216, insertC_out_gga(T211, T214, T216)) → insertC_out_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216))
U12_gga(T85, T86, T68, T69, T71, insertC_out_gga(s(T85), T68, T71)) → insertC_out_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69))
U10_gga(T76, T68, T69, T71, insertC_out_gga(0, T68, T71)) → insertC_out_gga(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69))
U8_gga(T42, T43, T44, T46, insertC_out_gga(T42, T44, T46)) → insertC_out_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46))
U3_gga(T28, T20, T23, insertC_out_gga(s(T28), T20, T23)) → pB_out_gga(T28, T20, T23)
U6_gga(T28, T20, T21, T23, pB_out_gga(T28, T20, T23)) → insertC_out_gga(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21))
INSERTC_IN_GGA(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21)) → U6_GGA(T28, T20, T21, T23, pB_in_gga(T28, T20, T23))
INSERTC_IN_GGA(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21)) → PB_IN_GGA(T28, T20, T23)
PB_IN_GGA(T28, T20, T23) → U2_GGA(T28, T20, T23, lessA_in_g(T28))
PB_IN_GGA(T28, T20, T23) → LESSA_IN_G(T28)
LESSA_IN_G(s(T31)) → U1_G(T31, lessA_in_g(T31))
LESSA_IN_G(s(T31)) → LESSA_IN_G(T31)
U2_GGA(T28, T20, T23, lessA_out_g(T28)) → U3_GGA(T28, T20, T23, insertC_in_gga(s(T28), T20, T23))
U2_GGA(T28, T20, T23, lessA_out_g(T28)) → INSERTC_IN_GGA(s(T28), T20, T23)
INSERTC_IN_GGA(T42, tree(T42, T43, T44), tree(T42, T43, T46)) → U7_GGA(T42, T43, T44, T46, lessA_in_g(T42))
INSERTC_IN_GGA(T42, tree(T42, T43, T44), tree(T42, T43, T46)) → LESSA_IN_G(T42)
U7_GGA(T42, T43, T44, T46, lessA_out_g(T42)) → U8_GGA(T42, T43, T44, T46, insertC_in_gga(T42, T44, T46))
U7_GGA(T42, T43, T44, T46, lessA_out_g(T42)) → INSERTC_IN_GGA(T42, T44, T46)
INSERTC_IN_GGA(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57)) → U9_GGA(T60, T54, T55, T57, pB_in_gga(T60, T55, T57))
INSERTC_IN_GGA(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57)) → PB_IN_GGA(T60, T55, T57)
INSERTC_IN_GGA(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69)) → U10_GGA(T76, T68, T69, T71, insertC_in_gga(0, T68, T71))
INSERTC_IN_GGA(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69)) → INSERTC_IN_GGA(0, T68, T71)
INSERTC_IN_GGA(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69)) → U11_GGA(T85, T86, T68, T69, T71, lessE_in_gg(T85, T86))
INSERTC_IN_GGA(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69)) → LESSE_IN_GG(T85, T86)
LESSE_IN_GG(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179)))))))) → U5_GG(T178, T179, lessD_in_gg(T178, T179))
LESSE_IN_GG(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179)))))))) → LESSD_IN_GG(T178, T179)
LESSD_IN_GG(s(T195), s(T196)) → U4_GG(T195, T196, lessD_in_gg(T195, T196))
LESSD_IN_GG(s(T195), s(T196)) → LESSD_IN_GG(T195, T196)
U11_GGA(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → U12_GGA(T85, T86, T68, T69, T71, insertC_in_gga(s(T85), T68, T71))
U11_GGA(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → INSERTC_IN_GGA(s(T85), T68, T71)
INSERTC_IN_GGA(T211, tree(T212, T213, T214), tree(T212, T213, T216)) → U13_GGA(T211, T212, T213, T214, T216, lessD_in_gg(T212, T211))
INSERTC_IN_GGA(T211, tree(T212, T213, T214), tree(T212, T213, T216)) → LESSD_IN_GG(T212, T211)
U13_GGA(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → U14_GGA(T211, T212, T213, T214, T216, insertC_in_gga(T211, T214, T216))
U13_GGA(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → INSERTC_IN_GGA(T211, T214, T216)
INSERTC_IN_GGA(s(T238), tree(0, T230, T231), tree(0, T230, T233)) → U15_GGA(T238, T230, T231, T233, insertC_in_gga(s(T238), T231, T233))
INSERTC_IN_GGA(s(T238), tree(0, T230, T231), tree(0, T230, T233)) → INSERTC_IN_GGA(s(T238), T231, T233)
INSERTC_IN_GGA(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233)) → U16_GGA(T246, T245, T230, T231, T233, lessD_in_gg(T245, T246))
INSERTC_IN_GGA(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233)) → LESSD_IN_GG(T245, T246)
U16_GGA(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → U17_GGA(T246, T245, T230, T231, T233, insertC_in_gga(s(T246), T231, T233))
U16_GGA(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → INSERTC_IN_GGA(s(T246), T231, T233)
insertC_in_gga(T5, void, tree(T5, void, void)) → insertC_out_gga(T5, void, tree(T5, void, void))
insertC_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertC_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertC_in_gga(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21)) → U6_gga(T28, T20, T21, T23, pB_in_gga(T28, T20, T23))
pB_in_gga(T28, T20, T23) → U2_gga(T28, T20, T23, lessA_in_g(T28))
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U2_gga(T28, T20, T23, lessA_out_g(T28)) → pB_out_gga(T28, T20, T23)
U2_gga(T28, T20, T23, lessA_out_g(T28)) → U3_gga(T28, T20, T23, insertC_in_gga(s(T28), T20, T23))
insertC_in_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46)) → U7_gga(T42, T43, T44, T46, lessA_in_g(T42))
U7_gga(T42, T43, T44, T46, lessA_out_g(T42)) → insertC_out_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46))
U7_gga(T42, T43, T44, T46, lessA_out_g(T42)) → U8_gga(T42, T43, T44, T46, insertC_in_gga(T42, T44, T46))
insertC_in_gga(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57)) → U9_gga(T60, T54, T55, T57, pB_in_gga(T60, T55, T57))
U9_gga(T60, T54, T55, T57, pB_out_gga(T60, T55, T57)) → insertC_out_gga(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57))
insertC_in_gga(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69)) → U10_gga(T76, T68, T69, T71, insertC_in_gga(0, T68, T71))
insertC_in_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69)) → U11_gga(T85, T86, T68, T69, T71, lessE_in_gg(T85, T86))
lessE_in_gg(0, s(T95)) → lessE_out_gg(0, s(T95))
lessE_in_gg(s(0), s(s(T108))) → lessE_out_gg(s(0), s(s(T108)))
lessE_in_gg(s(s(0)), s(s(s(T121)))) → lessE_out_gg(s(s(0)), s(s(s(T121))))
lessE_in_gg(s(s(s(0))), s(s(s(s(T134))))) → lessE_out_gg(s(s(s(0))), s(s(s(s(T134)))))
lessE_in_gg(s(s(s(s(0)))), s(s(s(s(s(T147)))))) → lessE_out_gg(s(s(s(s(0)))), s(s(s(s(s(T147))))))
lessE_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160))))))) → lessE_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160)))))))
lessE_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173)))))))) → lessE_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173))))))))
lessE_in_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179)))))))) → U5_gg(T178, T179, lessD_in_gg(T178, T179))
lessD_in_gg(0, s(T190)) → lessD_out_gg(0, s(T190))
lessD_in_gg(s(T195), s(T196)) → U4_gg(T195, T196, lessD_in_gg(T195, T196))
U4_gg(T195, T196, lessD_out_gg(T195, T196)) → lessD_out_gg(s(T195), s(T196))
U5_gg(T178, T179, lessD_out_gg(T178, T179)) → lessE_out_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179))))))))
U11_gga(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → insertC_out_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69))
U11_gga(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → U12_gga(T85, T86, T68, T69, T71, insertC_in_gga(s(T85), T68, T71))
insertC_in_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216)) → U13_gga(T211, T212, T213, T214, T216, lessD_in_gg(T212, T211))
U13_gga(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → insertC_out_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216))
U13_gga(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → U14_gga(T211, T212, T213, T214, T216, insertC_in_gga(T211, T214, T216))
insertC_in_gga(s(T238), tree(0, T230, T231), tree(0, T230, T233)) → U15_gga(T238, T230, T231, T233, insertC_in_gga(s(T238), T231, T233))
insertC_in_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233)) → U16_gga(T246, T245, T230, T231, T233, lessD_in_gg(T245, T246))
U16_gga(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → insertC_out_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233))
U16_gga(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → U17_gga(T246, T245, T230, T231, T233, insertC_in_gga(s(T246), T231, T233))
U17_gga(T246, T245, T230, T231, T233, insertC_out_gga(s(T246), T231, T233)) → insertC_out_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233))
U15_gga(T238, T230, T231, T233, insertC_out_gga(s(T238), T231, T233)) → insertC_out_gga(s(T238), tree(0, T230, T231), tree(0, T230, T233))
U14_gga(T211, T212, T213, T214, T216, insertC_out_gga(T211, T214, T216)) → insertC_out_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216))
U12_gga(T85, T86, T68, T69, T71, insertC_out_gga(s(T85), T68, T71)) → insertC_out_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69))
U10_gga(T76, T68, T69, T71, insertC_out_gga(0, T68, T71)) → insertC_out_gga(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69))
U8_gga(T42, T43, T44, T46, insertC_out_gga(T42, T44, T46)) → insertC_out_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46))
U3_gga(T28, T20, T23, insertC_out_gga(s(T28), T20, T23)) → pB_out_gga(T28, T20, T23)
U6_gga(T28, T20, T21, T23, pB_out_gga(T28, T20, T23)) → insertC_out_gga(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21))
LESSD_IN_GG(s(T195), s(T196)) → LESSD_IN_GG(T195, T196)
insertC_in_gga(T5, void, tree(T5, void, void)) → insertC_out_gga(T5, void, tree(T5, void, void))
insertC_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertC_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertC_in_gga(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21)) → U6_gga(T28, T20, T21, T23, pB_in_gga(T28, T20, T23))
pB_in_gga(T28, T20, T23) → U2_gga(T28, T20, T23, lessA_in_g(T28))
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U2_gga(T28, T20, T23, lessA_out_g(T28)) → pB_out_gga(T28, T20, T23)
U2_gga(T28, T20, T23, lessA_out_g(T28)) → U3_gga(T28, T20, T23, insertC_in_gga(s(T28), T20, T23))
insertC_in_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46)) → U7_gga(T42, T43, T44, T46, lessA_in_g(T42))
U7_gga(T42, T43, T44, T46, lessA_out_g(T42)) → insertC_out_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46))
U7_gga(T42, T43, T44, T46, lessA_out_g(T42)) → U8_gga(T42, T43, T44, T46, insertC_in_gga(T42, T44, T46))
insertC_in_gga(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57)) → U9_gga(T60, T54, T55, T57, pB_in_gga(T60, T55, T57))
U9_gga(T60, T54, T55, T57, pB_out_gga(T60, T55, T57)) → insertC_out_gga(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57))
insertC_in_gga(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69)) → U10_gga(T76, T68, T69, T71, insertC_in_gga(0, T68, T71))
insertC_in_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69)) → U11_gga(T85, T86, T68, T69, T71, lessE_in_gg(T85, T86))
lessE_in_gg(0, s(T95)) → lessE_out_gg(0, s(T95))
lessE_in_gg(s(0), s(s(T108))) → lessE_out_gg(s(0), s(s(T108)))
lessE_in_gg(s(s(0)), s(s(s(T121)))) → lessE_out_gg(s(s(0)), s(s(s(T121))))
lessE_in_gg(s(s(s(0))), s(s(s(s(T134))))) → lessE_out_gg(s(s(s(0))), s(s(s(s(T134)))))
lessE_in_gg(s(s(s(s(0)))), s(s(s(s(s(T147)))))) → lessE_out_gg(s(s(s(s(0)))), s(s(s(s(s(T147))))))
lessE_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160))))))) → lessE_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160)))))))
lessE_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173)))))))) → lessE_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173))))))))
lessE_in_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179)))))))) → U5_gg(T178, T179, lessD_in_gg(T178, T179))
lessD_in_gg(0, s(T190)) → lessD_out_gg(0, s(T190))
lessD_in_gg(s(T195), s(T196)) → U4_gg(T195, T196, lessD_in_gg(T195, T196))
U4_gg(T195, T196, lessD_out_gg(T195, T196)) → lessD_out_gg(s(T195), s(T196))
U5_gg(T178, T179, lessD_out_gg(T178, T179)) → lessE_out_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179))))))))
U11_gga(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → insertC_out_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69))
U11_gga(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → U12_gga(T85, T86, T68, T69, T71, insertC_in_gga(s(T85), T68, T71))
insertC_in_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216)) → U13_gga(T211, T212, T213, T214, T216, lessD_in_gg(T212, T211))
U13_gga(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → insertC_out_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216))
U13_gga(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → U14_gga(T211, T212, T213, T214, T216, insertC_in_gga(T211, T214, T216))
insertC_in_gga(s(T238), tree(0, T230, T231), tree(0, T230, T233)) → U15_gga(T238, T230, T231, T233, insertC_in_gga(s(T238), T231, T233))
insertC_in_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233)) → U16_gga(T246, T245, T230, T231, T233, lessD_in_gg(T245, T246))
U16_gga(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → insertC_out_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233))
U16_gga(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → U17_gga(T246, T245, T230, T231, T233, insertC_in_gga(s(T246), T231, T233))
U17_gga(T246, T245, T230, T231, T233, insertC_out_gga(s(T246), T231, T233)) → insertC_out_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233))
U15_gga(T238, T230, T231, T233, insertC_out_gga(s(T238), T231, T233)) → insertC_out_gga(s(T238), tree(0, T230, T231), tree(0, T230, T233))
U14_gga(T211, T212, T213, T214, T216, insertC_out_gga(T211, T214, T216)) → insertC_out_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216))
U12_gga(T85, T86, T68, T69, T71, insertC_out_gga(s(T85), T68, T71)) → insertC_out_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69))
U10_gga(T76, T68, T69, T71, insertC_out_gga(0, T68, T71)) → insertC_out_gga(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69))
U8_gga(T42, T43, T44, T46, insertC_out_gga(T42, T44, T46)) → insertC_out_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46))
U3_gga(T28, T20, T23, insertC_out_gga(s(T28), T20, T23)) → pB_out_gga(T28, T20, T23)
U6_gga(T28, T20, T21, T23, pB_out_gga(T28, T20, T23)) → insertC_out_gga(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21))
LESSD_IN_GG(s(T195), s(T196)) → LESSD_IN_GG(T195, T196)
LESSD_IN_GG(s(T195), s(T196)) → LESSD_IN_GG(T195, T196)
From the DPs we obtained the following set of size-change graphs:
LESSA_IN_G(s(T31)) → LESSA_IN_G(T31)
insertC_in_gga(T5, void, tree(T5, void, void)) → insertC_out_gga(T5, void, tree(T5, void, void))
insertC_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertC_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertC_in_gga(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21)) → U6_gga(T28, T20, T21, T23, pB_in_gga(T28, T20, T23))
pB_in_gga(T28, T20, T23) → U2_gga(T28, T20, T23, lessA_in_g(T28))
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U2_gga(T28, T20, T23, lessA_out_g(T28)) → pB_out_gga(T28, T20, T23)
U2_gga(T28, T20, T23, lessA_out_g(T28)) → U3_gga(T28, T20, T23, insertC_in_gga(s(T28), T20, T23))
insertC_in_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46)) → U7_gga(T42, T43, T44, T46, lessA_in_g(T42))
U7_gga(T42, T43, T44, T46, lessA_out_g(T42)) → insertC_out_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46))
U7_gga(T42, T43, T44, T46, lessA_out_g(T42)) → U8_gga(T42, T43, T44, T46, insertC_in_gga(T42, T44, T46))
insertC_in_gga(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57)) → U9_gga(T60, T54, T55, T57, pB_in_gga(T60, T55, T57))
U9_gga(T60, T54, T55, T57, pB_out_gga(T60, T55, T57)) → insertC_out_gga(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57))
insertC_in_gga(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69)) → U10_gga(T76, T68, T69, T71, insertC_in_gga(0, T68, T71))
insertC_in_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69)) → U11_gga(T85, T86, T68, T69, T71, lessE_in_gg(T85, T86))
lessE_in_gg(0, s(T95)) → lessE_out_gg(0, s(T95))
lessE_in_gg(s(0), s(s(T108))) → lessE_out_gg(s(0), s(s(T108)))
lessE_in_gg(s(s(0)), s(s(s(T121)))) → lessE_out_gg(s(s(0)), s(s(s(T121))))
lessE_in_gg(s(s(s(0))), s(s(s(s(T134))))) → lessE_out_gg(s(s(s(0))), s(s(s(s(T134)))))
lessE_in_gg(s(s(s(s(0)))), s(s(s(s(s(T147)))))) → lessE_out_gg(s(s(s(s(0)))), s(s(s(s(s(T147))))))
lessE_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160))))))) → lessE_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160)))))))
lessE_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173)))))))) → lessE_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173))))))))
lessE_in_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179)))))))) → U5_gg(T178, T179, lessD_in_gg(T178, T179))
lessD_in_gg(0, s(T190)) → lessD_out_gg(0, s(T190))
lessD_in_gg(s(T195), s(T196)) → U4_gg(T195, T196, lessD_in_gg(T195, T196))
U4_gg(T195, T196, lessD_out_gg(T195, T196)) → lessD_out_gg(s(T195), s(T196))
U5_gg(T178, T179, lessD_out_gg(T178, T179)) → lessE_out_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179))))))))
U11_gga(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → insertC_out_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69))
U11_gga(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → U12_gga(T85, T86, T68, T69, T71, insertC_in_gga(s(T85), T68, T71))
insertC_in_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216)) → U13_gga(T211, T212, T213, T214, T216, lessD_in_gg(T212, T211))
U13_gga(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → insertC_out_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216))
U13_gga(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → U14_gga(T211, T212, T213, T214, T216, insertC_in_gga(T211, T214, T216))
insertC_in_gga(s(T238), tree(0, T230, T231), tree(0, T230, T233)) → U15_gga(T238, T230, T231, T233, insertC_in_gga(s(T238), T231, T233))
insertC_in_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233)) → U16_gga(T246, T245, T230, T231, T233, lessD_in_gg(T245, T246))
U16_gga(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → insertC_out_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233))
U16_gga(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → U17_gga(T246, T245, T230, T231, T233, insertC_in_gga(s(T246), T231, T233))
U17_gga(T246, T245, T230, T231, T233, insertC_out_gga(s(T246), T231, T233)) → insertC_out_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233))
U15_gga(T238, T230, T231, T233, insertC_out_gga(s(T238), T231, T233)) → insertC_out_gga(s(T238), tree(0, T230, T231), tree(0, T230, T233))
U14_gga(T211, T212, T213, T214, T216, insertC_out_gga(T211, T214, T216)) → insertC_out_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216))
U12_gga(T85, T86, T68, T69, T71, insertC_out_gga(s(T85), T68, T71)) → insertC_out_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69))
U10_gga(T76, T68, T69, T71, insertC_out_gga(0, T68, T71)) → insertC_out_gga(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69))
U8_gga(T42, T43, T44, T46, insertC_out_gga(T42, T44, T46)) → insertC_out_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46))
U3_gga(T28, T20, T23, insertC_out_gga(s(T28), T20, T23)) → pB_out_gga(T28, T20, T23)
U6_gga(T28, T20, T21, T23, pB_out_gga(T28, T20, T23)) → insertC_out_gga(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21))
LESSA_IN_G(s(T31)) → LESSA_IN_G(T31)
LESSA_IN_G(s(T31)) → LESSA_IN_G(T31)
From the DPs we obtained the following set of size-change graphs:
INSERTC_IN_GGA(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21)) → PB_IN_GGA(T28, T20, T23)
PB_IN_GGA(T28, T20, T23) → U2_GGA(T28, T20, T23, lessA_in_g(T28))
U2_GGA(T28, T20, T23, lessA_out_g(T28)) → INSERTC_IN_GGA(s(T28), T20, T23)
INSERTC_IN_GGA(T42, tree(T42, T43, T44), tree(T42, T43, T46)) → U7_GGA(T42, T43, T44, T46, lessA_in_g(T42))
U7_GGA(T42, T43, T44, T46, lessA_out_g(T42)) → INSERTC_IN_GGA(T42, T44, T46)
INSERTC_IN_GGA(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57)) → PB_IN_GGA(T60, T55, T57)
INSERTC_IN_GGA(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69)) → INSERTC_IN_GGA(0, T68, T71)
INSERTC_IN_GGA(T211, tree(T212, T213, T214), tree(T212, T213, T216)) → U13_GGA(T211, T212, T213, T214, T216, lessD_in_gg(T212, T211))
U13_GGA(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → INSERTC_IN_GGA(T211, T214, T216)
INSERTC_IN_GGA(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69)) → U11_GGA(T85, T86, T68, T69, T71, lessE_in_gg(T85, T86))
U11_GGA(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → INSERTC_IN_GGA(s(T85), T68, T71)
INSERTC_IN_GGA(s(T238), tree(0, T230, T231), tree(0, T230, T233)) → INSERTC_IN_GGA(s(T238), T231, T233)
INSERTC_IN_GGA(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233)) → U16_GGA(T246, T245, T230, T231, T233, lessD_in_gg(T245, T246))
U16_GGA(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → INSERTC_IN_GGA(s(T246), T231, T233)
insertC_in_gga(T5, void, tree(T5, void, void)) → insertC_out_gga(T5, void, tree(T5, void, void))
insertC_in_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14)) → insertC_out_gga(T12, tree(T12, T13, T14), tree(T12, T13, T14))
insertC_in_gga(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21)) → U6_gga(T28, T20, T21, T23, pB_in_gga(T28, T20, T23))
pB_in_gga(T28, T20, T23) → U2_gga(T28, T20, T23, lessA_in_g(T28))
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U2_gga(T28, T20, T23, lessA_out_g(T28)) → pB_out_gga(T28, T20, T23)
U2_gga(T28, T20, T23, lessA_out_g(T28)) → U3_gga(T28, T20, T23, insertC_in_gga(s(T28), T20, T23))
insertC_in_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46)) → U7_gga(T42, T43, T44, T46, lessA_in_g(T42))
U7_gga(T42, T43, T44, T46, lessA_out_g(T42)) → insertC_out_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46))
U7_gga(T42, T43, T44, T46, lessA_out_g(T42)) → U8_gga(T42, T43, T44, T46, insertC_in_gga(T42, T44, T46))
insertC_in_gga(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57)) → U9_gga(T60, T54, T55, T57, pB_in_gga(T60, T55, T57))
U9_gga(T60, T54, T55, T57, pB_out_gga(T60, T55, T57)) → insertC_out_gga(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57))
insertC_in_gga(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69)) → U10_gga(T76, T68, T69, T71, insertC_in_gga(0, T68, T71))
insertC_in_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69)) → U11_gga(T85, T86, T68, T69, T71, lessE_in_gg(T85, T86))
lessE_in_gg(0, s(T95)) → lessE_out_gg(0, s(T95))
lessE_in_gg(s(0), s(s(T108))) → lessE_out_gg(s(0), s(s(T108)))
lessE_in_gg(s(s(0)), s(s(s(T121)))) → lessE_out_gg(s(s(0)), s(s(s(T121))))
lessE_in_gg(s(s(s(0))), s(s(s(s(T134))))) → lessE_out_gg(s(s(s(0))), s(s(s(s(T134)))))
lessE_in_gg(s(s(s(s(0)))), s(s(s(s(s(T147)))))) → lessE_out_gg(s(s(s(s(0)))), s(s(s(s(s(T147))))))
lessE_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160))))))) → lessE_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160)))))))
lessE_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173)))))))) → lessE_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173))))))))
lessE_in_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179)))))))) → U5_gg(T178, T179, lessD_in_gg(T178, T179))
lessD_in_gg(0, s(T190)) → lessD_out_gg(0, s(T190))
lessD_in_gg(s(T195), s(T196)) → U4_gg(T195, T196, lessD_in_gg(T195, T196))
U4_gg(T195, T196, lessD_out_gg(T195, T196)) → lessD_out_gg(s(T195), s(T196))
U5_gg(T178, T179, lessD_out_gg(T178, T179)) → lessE_out_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179))))))))
U11_gga(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → insertC_out_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69))
U11_gga(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → U12_gga(T85, T86, T68, T69, T71, insertC_in_gga(s(T85), T68, T71))
insertC_in_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216)) → U13_gga(T211, T212, T213, T214, T216, lessD_in_gg(T212, T211))
U13_gga(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → insertC_out_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216))
U13_gga(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → U14_gga(T211, T212, T213, T214, T216, insertC_in_gga(T211, T214, T216))
insertC_in_gga(s(T238), tree(0, T230, T231), tree(0, T230, T233)) → U15_gga(T238, T230, T231, T233, insertC_in_gga(s(T238), T231, T233))
insertC_in_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233)) → U16_gga(T246, T245, T230, T231, T233, lessD_in_gg(T245, T246))
U16_gga(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → insertC_out_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233))
U16_gga(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → U17_gga(T246, T245, T230, T231, T233, insertC_in_gga(s(T246), T231, T233))
U17_gga(T246, T245, T230, T231, T233, insertC_out_gga(s(T246), T231, T233)) → insertC_out_gga(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233))
U15_gga(T238, T230, T231, T233, insertC_out_gga(s(T238), T231, T233)) → insertC_out_gga(s(T238), tree(0, T230, T231), tree(0, T230, T233))
U14_gga(T211, T212, T213, T214, T216, insertC_out_gga(T211, T214, T216)) → insertC_out_gga(T211, tree(T212, T213, T214), tree(T212, T213, T216))
U12_gga(T85, T86, T68, T69, T71, insertC_out_gga(s(T85), T68, T71)) → insertC_out_gga(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69))
U10_gga(T76, T68, T69, T71, insertC_out_gga(0, T68, T71)) → insertC_out_gga(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69))
U8_gga(T42, T43, T44, T46, insertC_out_gga(T42, T44, T46)) → insertC_out_gga(T42, tree(T42, T43, T44), tree(T42, T43, T46))
U3_gga(T28, T20, T23, insertC_out_gga(s(T28), T20, T23)) → pB_out_gga(T28, T20, T23)
U6_gga(T28, T20, T21, T23, pB_out_gga(T28, T20, T23)) → insertC_out_gga(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21))
INSERTC_IN_GGA(s(T28), tree(s(T28), T20, T21), tree(s(T28), T23, T21)) → PB_IN_GGA(T28, T20, T23)
PB_IN_GGA(T28, T20, T23) → U2_GGA(T28, T20, T23, lessA_in_g(T28))
U2_GGA(T28, T20, T23, lessA_out_g(T28)) → INSERTC_IN_GGA(s(T28), T20, T23)
INSERTC_IN_GGA(T42, tree(T42, T43, T44), tree(T42, T43, T46)) → U7_GGA(T42, T43, T44, T46, lessA_in_g(T42))
U7_GGA(T42, T43, T44, T46, lessA_out_g(T42)) → INSERTC_IN_GGA(T42, T44, T46)
INSERTC_IN_GGA(s(T60), tree(s(T60), T54, T55), tree(s(T60), T54, T57)) → PB_IN_GGA(T60, T55, T57)
INSERTC_IN_GGA(0, tree(s(T76), T68, T69), tree(s(T76), T71, T69)) → INSERTC_IN_GGA(0, T68, T71)
INSERTC_IN_GGA(T211, tree(T212, T213, T214), tree(T212, T213, T216)) → U13_GGA(T211, T212, T213, T214, T216, lessD_in_gg(T212, T211))
U13_GGA(T211, T212, T213, T214, T216, lessD_out_gg(T212, T211)) → INSERTC_IN_GGA(T211, T214, T216)
INSERTC_IN_GGA(s(T85), tree(s(T86), T68, T69), tree(s(T86), T71, T69)) → U11_GGA(T85, T86, T68, T69, T71, lessE_in_gg(T85, T86))
U11_GGA(T85, T86, T68, T69, T71, lessE_out_gg(T85, T86)) → INSERTC_IN_GGA(s(T85), T68, T71)
INSERTC_IN_GGA(s(T238), tree(0, T230, T231), tree(0, T230, T233)) → INSERTC_IN_GGA(s(T238), T231, T233)
INSERTC_IN_GGA(s(T246), tree(s(T245), T230, T231), tree(s(T245), T230, T233)) → U16_GGA(T246, T245, T230, T231, T233, lessD_in_gg(T245, T246))
U16_GGA(T246, T245, T230, T231, T233, lessD_out_gg(T245, T246)) → INSERTC_IN_GGA(s(T246), T231, T233)
lessA_in_g(s(T31)) → U1_g(T31, lessA_in_g(T31))
lessD_in_gg(0, s(T190)) → lessD_out_gg(0, s(T190))
lessD_in_gg(s(T195), s(T196)) → U4_gg(T195, T196, lessD_in_gg(T195, T196))
lessE_in_gg(0, s(T95)) → lessE_out_gg(0, s(T95))
lessE_in_gg(s(0), s(s(T108))) → lessE_out_gg(s(0), s(s(T108)))
lessE_in_gg(s(s(0)), s(s(s(T121)))) → lessE_out_gg(s(s(0)), s(s(s(T121))))
lessE_in_gg(s(s(s(0))), s(s(s(s(T134))))) → lessE_out_gg(s(s(s(0))), s(s(s(s(T134)))))
lessE_in_gg(s(s(s(s(0)))), s(s(s(s(s(T147)))))) → lessE_out_gg(s(s(s(s(0)))), s(s(s(s(s(T147))))))
lessE_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160))))))) → lessE_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160)))))))
lessE_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173)))))))) → lessE_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173))))))))
lessE_in_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179)))))))) → U5_gg(T178, T179, lessD_in_gg(T178, T179))
U1_g(T31, lessA_out_g(T31)) → lessA_out_g(s(T31))
U4_gg(T195, T196, lessD_out_gg(T195, T196)) → lessD_out_gg(s(T195), s(T196))
U5_gg(T178, T179, lessD_out_gg(T178, T179)) → lessE_out_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179))))))))
INSERTC_IN_GGA(s(T28), tree(s(T28), T20, T21)) → PB_IN_GGA(T28, T20)
PB_IN_GGA(T28, T20) → U2_GGA(T28, T20, lessA_in_g(T28))
U2_GGA(T28, T20, lessA_out_g) → INSERTC_IN_GGA(s(T28), T20)
INSERTC_IN_GGA(T42, tree(T42, T43, T44)) → U7_GGA(T42, T44, lessA_in_g(T42))
U7_GGA(T42, T44, lessA_out_g) → INSERTC_IN_GGA(T42, T44)
INSERTC_IN_GGA(s(T60), tree(s(T60), T54, T55)) → PB_IN_GGA(T60, T55)
INSERTC_IN_GGA(0, tree(s(T76), T68, T69)) → INSERTC_IN_GGA(0, T68)
INSERTC_IN_GGA(T211, tree(T212, T213, T214)) → U13_GGA(T211, T214, lessD_in_gg(T212, T211))
U13_GGA(T211, T214, lessD_out_gg) → INSERTC_IN_GGA(T211, T214)
INSERTC_IN_GGA(s(T85), tree(s(T86), T68, T69)) → U11_GGA(T85, T68, lessE_in_gg(T85, T86))
U11_GGA(T85, T68, lessE_out_gg) → INSERTC_IN_GGA(s(T85), T68)
INSERTC_IN_GGA(s(T238), tree(0, T230, T231)) → INSERTC_IN_GGA(s(T238), T231)
INSERTC_IN_GGA(s(T246), tree(s(T245), T230, T231)) → U16_GGA(T246, T231, lessD_in_gg(T245, T246))
U16_GGA(T246, T231, lessD_out_gg) → INSERTC_IN_GGA(s(T246), T231)
lessA_in_g(s(T31)) → U1_g(lessA_in_g(T31))
lessD_in_gg(0, s(T190)) → lessD_out_gg
lessD_in_gg(s(T195), s(T196)) → U4_gg(lessD_in_gg(T195, T196))
lessE_in_gg(0, s(T95)) → lessE_out_gg
lessE_in_gg(s(0), s(s(T108))) → lessE_out_gg
lessE_in_gg(s(s(0)), s(s(s(T121)))) → lessE_out_gg
lessE_in_gg(s(s(s(0))), s(s(s(s(T134))))) → lessE_out_gg
lessE_in_gg(s(s(s(s(0)))), s(s(s(s(s(T147)))))) → lessE_out_gg
lessE_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T160))))))) → lessE_out_gg
lessE_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T173)))))))) → lessE_out_gg
lessE_in_gg(s(s(s(s(s(s(s(T178))))))), s(s(s(s(s(s(s(T179)))))))) → U5_gg(lessD_in_gg(T178, T179))
U1_g(lessA_out_g) → lessA_out_g
U4_gg(lessD_out_gg) → lessD_out_gg
U5_gg(lessD_out_gg) → lessE_out_gg
lessA_in_g(x0)
lessD_in_gg(x0, x1)
lessE_in_gg(x0, x1)
U1_g(x0)
U4_gg(x0)
U5_gg(x0)
From the DPs we obtained the following set of size-change graphs: